$a$ in dom($M$.pre) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\uparrow$fpf{-}dom(IdDeq; $a$; (($M$.2.2.2).1))